Refinement Calculus
-------------------

<!--
SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.

SPDX-License-Identifier: CC0-1.0
-->

[(Up)](../../README.md#topics) | _See also: [Logic](../Logic/README.md#logic), [Formal Specification](../Formal%20Specification/README.md#formal-specification), [Theorem Proving](../Theorem%20Proving/README.md#theorem-proving)_

- - - -


### Web resources

[Refinement Calculus](https://www.southampton.ac.uk/~mbutler/refcalc-tut/home.html) ★★★

[The Retrenchment Homepage](http://www.cs.man.ac.uk/~banach/retrenchment/) ★

_(in [Relational Programming](../Relational%20Programming/README.md#relational-programming))_ [A Short Skinny on Relations & the Algebra of Programming | Hey There Buddo!](https://www.philipzucker.com/a-short-skinny-on-relations-towards-the-algebra-of-programming/) ★★★


### Papers

Can Programming Be Liberated from the von Neumann Style? (online @ [dl.acm.org](https://dl.acm.org/doi/10.1145/359576.359579)) 🏛️ [💭](commentary/Chris%20Pressey.md#can-programming-be-liberated-from-the-von-neumann-style)

Algorithmics (online @ [ir.cwi.nl](https://ir.cwi.nl/pub/2686/2686D.pdf), [www.kestrel.edu](https://www.kestrel.edu/people/meertens/publications/papers/Algorithmics.pdf)) ★★★ [💭](commentary/Chris%20Pressey.md#algorithmics)

Laws of Programming (online @ [ox.ac.uk](https://www.cs.ox.ac.uk/bill.roscoe/publications/20.pdf)) ★★★ [💭](commentary/Chris%20Pressey.md#laws-of-programming)

Algebraic Identities for Program Calculation (online @ [academic.oup.com](https://academic.oup.com/comjnl/article-pdf/32/2/122/1445670/320122.pdf)) ★★★ [💭](commentary/Chris%20Pressey.md#algebraic-identities-for-program-calculation)

The specification statement (online @ [dl.acm.org](https://dl.acm.org/doi/10.1145/44501.44503)) 🏛️

Correctness Preserving Program Refinements (online @ [ir.cwl.nl](https://ir.cwi.nl/pub/12990))

[Program Derivation by Correctness Enhancements](https://arxiv.org/abs/1606.02020)


### Books

Programming from Specifications (online @ [www.cs.ox.ac.uk](https://www.cs.ox.ac.uk/publications/books/PfS/)) ★ [💭](commentary/Chris%20Pressey.md#programming-from-specifications)

a Practical Theory of Programming (online @ [www.cs.toronto.edu](https://www.cs.toronto.edu/~hehner/aPToP/))

Refinement Calculus: A Systematic Introduction (online @ [lara.epfl.ch](https://lara.epfl.ch/w/_media/sav08:backwright98refinementcalculus.pdf)) [💭](commentary/Chris%20Pressey.md#refinement-calculus-a-systematic-introduction)